In this notebook, we will compute the stable coefficients of the census knots or prove that there exist no compatible stable coefficients (and compute N if they exist) and thus obstruct some knots in the SnapPy census from having alternating surgeries.

In [1]:
import snappy
import time
import csv

def torsion_coef(knot):
    '''
    A function that takes the name of a knot and return the torsion coefficients of its normalized Alexander polynomial.
    '''
    M=snappy.Manifold(knot)
    a=M.alexander_polynomial().list()
    t=[]
    for i in range(0,len(a)):
        ti=0
        for j in range(0,len(a)-i):
            ti=ti+j*a[j+i]
        t.append(ti)
        # Next we need to adjust for the correct normalization of the Alexander polynomial
    g=int((len(t)-1)/2)
    r=t[g:2*g]
    T=[]
    Ti=0
    for i in range(1,r[0]+1):
        Ti=r.count(i)+Ti
        T.append(Ti)
    return T

## This code calculates the stable coefficients given the torsion
## coefficients. If no stable coefficients can exist it will return False.
## It takes as input the list [T_1, \dots, T_{t0}]. Where T_k is defined
## as the number if 0\leq i <g such that t_i\leq k.

def Generate_S(n):
    ##Generate the tuples S_k for k=0 to n.
    S=[]
    for k in range(0,n+1):
        S+=[[]]
        j=1
        while j*(j+1)<2*k:
            for t in S[k-(j*(j+1))//2]:
                if j>=t[0]:
                    S[k]+=[[j]+t]
            j+=1

        if j*(j+1)==2*k:
            S[k]+=[[j]]

    return S

def max_pairing(sigma, Sk):
    ##compute max \sigma \cdot \alpha for all \alpha in Sk
    prodlist = [sum([z[0]*z[1] for z in zip(alpha, sigma)]) for alpha in Sk]
    return max(prodlist)

def Calc_Stable(Tlist):
    ##Take the tuple of T_i and determine whether there exists a
    ##tuple of stable coefficients consistent with this.
    t0=len(Tlist)
    g=Tlist[-1]

    ##For indexing reasons append a 0 to the start.
    T=[0]+Tlist
    rho=[]
 
    S=Generate_S(t0)
    k=1
    ##Calculate the \rho_i greater than 2.
    while k<=t0 and T[k]-T[k-1]>2:
        if max_pairing(rho,S[k])<T[k]:
            rho+=[T[k]-T[k-1]]
        ##Check rho decreasing
        if k>1 and rho[-1]>rho[-2]:
            return False
        k+=1

    ##Fill out rho with 2s.
    gsum=sum([(x*(x-1))//2 for x in rho])

    if gsum>g:
        return False
    rho+=[2]*(g-gsum)
    
    ##Finally check that rho is compatible with the T we started with.
    ##pad out rho with some entries equal to one and compute the
    ##relevant maxima.
    sigma=rho+[1]*t0
    for k in range(1,t0):
        if T[k]!=max_pairing(sigma,S[k]):
            return False
    if max_pairing(sigma,S[t0])<g:
        return False
    
    return rho
                 
##print(Calc_Stable([3,5]))
##
##m=[11, 16, 22, 27, 32, 37, 38, 43, 48, 49, 53, 54, 59, 60, 64, 65, 69, 70, 74, 75, 76, 80, 81, 85]
##print(m)
##print(Calc_Stable(m))
##
##tests=[[1],[2],[3],[4],[2,3],[2,3,4],[2,4,5],[3,6],[3,6,9],[3,6,10],[3,4],[4,5],[4,5,6],[4,7,8,9],[4,7,8,9,10],
##       [4,6,8,10],[4,7,8,9],[4,7,8,10],[3,6,7],[3,6,8],[3,6,8,10],[4,7,9,12],
##       [5,9,12,15,17,20,21,22],[7,12,15,19,21,24,27,28,31,33],
##       [5,8,11,13,15,16],[6,9,12,15,17,19,21], [5,7,10,12,13],
##       [6,9,12,15,17,19],[2,6,7]]
##
##for T in tests:
##    print(T, Calc_Stable(T))

## ##Torsion lists for the unknown L-space knots
##T=[8,11,16,19,21,24,27,29,31,33,34]
##T=[8,13,16,21,24,27,30,32,35,36,38,40,42,43]
##print(Calc_Stable(T))


def compute_N(stable_coefficients):
    '''
    Takes as input the stable coefficients and returns the integer N.
    '''
    N=0
    stable_coefficients=sorted(stable_coefficients)
    for s in stable_coefficients:
        N=N+s*s
    values=[]
    for s in stable_coefficients:
        value=s
        for x in stable_coefficients[0:stable_coefficients.index(s)]:
            value=value-x
        values.append(value)
    return N+max(values)
In [2]:
LSpaceKnots=[]
with open('census_L_space_knots.csv', 'r') as file:
    reader = csv.reader(file)
    for row in reader:
        LSpaceKnots.append(row[0])
        
LSpaceKnots=LSpaceKnots[1:]

len(LSpaceKnots)
Out[2]:
632
In [3]:
start_time = time.time()
census_knots_without_alternating_surgery=[]
census_knots_with_stable_coefficients=[]

for knot in LSpaceKnots:
    T=torsion_coef(knot)
    stab=Calc_Stable(T)
    if stab==False:
        census_knots_without_alternating_surgery.append(knot)
    else:
        census_knots_with_stable_coefficients.append([knot,stab,compute_N(stab)])    

print('Number of L-space census knots without alternating surgeries:',len(census_knots_without_alternating_surgery))
print('Number of L-space census knots with stable coefficients:',len(census_knots_with_stable_coefficients))
print("--- Time taken: %s seconds ---" % ((time.time() - start_time)))

Number of L-space census knots without alternating surgeries: 124
Number of L-space census knots with stable coefficients: 508
--- Time taken: 2.1052589416503906 seconds ---

We print and save the data:

In [4]:
with open("stable_coefficients.csv", "a") as output: #Opens output file # Use the a parameter to add a row
    csvwriter = csv.writer(output, delimiter = ",")
    csvwriter.writerow(('knot','stable coefficients','N'))

for x in census_knots_with_stable_coefficients:
    with open("stable_coefficients.csv", "a") as output: #Opens output file # Use the a parameter to add a row
        csvwriter = csv.writer(output, delimiter = ",")
        csvwriter.writerow((x[0],x[1],x[2]))
In [5]:
census_knots_with_stable_coefficients
Out[5]:
[['m016', [3, 2, 2], 19],
 ['m071', [5, 2], 32],
 ['m082', [3, 3, 2, 2], 28],
 ['m103', [5, 3, 2, 2], 44],
 ['m118', [4, 3, 2], 31],
 ['m144', [3, 3, 3, 2, 2], 37],
 ['m194', [5, 3], 37],
 ['m198', [5, 2, 2, 2], 39],
 ['m223', [3, 2, 2, 2], 23],
 ['m239', [4, 3, 2, 2], 35],
 ['m240', [4, 3, 3], 37],
 ['m270', [5, 3, 3], 46],
 ['m276', [5, 4, 2, 2], 51],
 ['m281', [4, 4, 3, 2], 47],
 ['o9_00133', [5, 5, 5, 5, 5, 2], 132],
 ['o9_00168', [5, 5, 5, 5, 5, 3, 2, 2], 144],
 ['o9_00644', [3, 3, 3, 3, 3, 3, 3, 2, 2], 73],
 ['o9_00797', [7, 7, 7, 7, 3, 2, 2], 215],
 ['o9_00815', [7, 7, 7, 7, 4, 3, 2], 227],
 ['o9_01079', [6, 6, 6, 2], 116],
 ['o9_01436', [7, 7, 7, 2, 2], 158],
 ['o9_01496', [7, 7, 7, 5, 2, 2, 2], 186],
 ['o9_01584', [8, 8, 8, 3, 3, 2, 2], 220],
 ['o9_01621', [8, 8, 8, 5, 3], 229],
 ['o9_01680', [8, 8, 8, 3, 2, 2], 211],
 ['o9_01765', [8, 8, 8, 5, 3, 3], 238],
 ['o9_01936', [7, 2], 58],
 ['o9_01953', [5, 5, 5, 5, 5, 3], 137],
 ['o9_01955', [5, 5, 5, 5, 5, 2, 2, 2], 139],
 ['o9_02255', [10, 10, 3, 3, 2, 2], 228],
 ['o9_02340', [10, 10, 4, 3, 3], 237],
 ['o9_02350', [10, 10, 7, 3, 3, 2], 273],
 ['o9_02386', [10, 10, 6, 4, 3], 264],
 ['o9_02655', [9, 9, 4, 3, 2, 2], 197],
 ['o9_02696', [9, 9, 5, 4, 2], 209],
 ['o9_02706', [9, 9, 9, 4, 3, 2], 274],
 ['o9_02735', [9, 9, 9, 5, 4, 2, 2], 294],
 ['o9_02772', [9, 2, 2, 2], 96],
 ['o9_02786', [4, 4, 4, 4, 4, 3, 2, 2], 99],
 ['o9_02794', [4, 4, 4, 4, 4, 4, 3, 2], 111],
 ['o9_03032', [9, 7, 2, 2, 2, 2], 148],
 ['o9_03108', [9, 2, 2, 2, 2, 2], 103],
 ['o9_03118', [11, 11, 5, 4, 2, 2], 293],
 ['o9_03133', [11, 3, 3, 3, 2, 2], 158],
 ['o9_03149', [11, 11, 6, 5, 2, 2], 313],
 ['o9_03162', [11, 11, 4, 4, 3, 2], 289],
 ['o9_03188', [11, 11, 7, 4, 2, 2], 317],
 ['o9_03288', [11, 4, 3, 3], 158],
 ['o9_03313', [11, 8, 3, 3], 206],
 ['o9_03412', [11, 7, 4, 4], 206],
 ['o9_03526', [6, 5, 5], 91],
 ['o9_03586', [7, 7, 7, 2, 2, 2, 2], 165],
 ['o9_03622', [7, 7, 7, 5, 2], 179],
 ['o9_03802', [11, 3, 3, 3], 151],
 ['o9_03833', [9, 7, 2, 2], 141],
 ['o9_03932', [9, 5, 5], 136],
 ['o9_04106', [12, 5, 5, 2, 2, 2], 208],
 ['o9_04205', [12, 7, 5, 2], 225],
 ['o9_04245', [13, 5, 5, 3], 231],
 ['o9_04269', [5, 5, 5, 5, 4, 2], 122],
 ['o9_04313', [13, 6, 5, 2, 2], 240],
 ['o9_04431', [13, 7, 6, 2, 2, 2], 268],
 ['o9_04435', [9, 8, 2, 2, 2, 2], 163],
 ['o9_04438', [13, 8, 5, 3, 2, 2], 277],
 ['o9_04938', [6, 6, 5, 2], 104],
 ['o9_05021', [8, 8, 8, 3, 3], 213],
 ['o9_05177', [8, 8, 8, 5, 3, 2, 2], 236],
 ['o9_05229', [12, 5, 5, 2], 201],
 ['o9_05287', [3, 2, 2, 2, 2, 2, 2, 2], 39],
 ['o9_05357', [11, 8, 3, 3, 2, 2], 213],
 ['o9_05426', [7, 7, 7, 7, 3, 3, 2], 220],
 ['o9_05483', [7, 7, 7, 7, 4, 2, 2], 222],
 ['o9_05562', [13, 5, 5, 3, 2, 2], 238],
 ['o9_05618', [12, 7, 5, 2, 2, 2], 232],
 ['o9_05860', [10, 10, 3, 3, 3, 2], 233],
 ['o9_05970', [13, 8, 5, 3], 270],
 ['o9_06060', [9, 9, 4, 4, 2], 200],
 ['o9_06128', [10, 10, 7, 3, 2, 2], 268],
 ['o9_06154', [9, 9, 5, 3, 2, 2], 206],
 ['o9_06248', [11, 11, 4, 4, 2, 2], 284],
 ['o9_06301', [11, 11, 7, 4, 3, 2], 322],
 ['o9_06956', [9, 3, 2, 2, 2], 104],
 ['o9_07167', [8, 2, 2], 76],
 ['o9_07195', [10, 6, 4], 156],
 ['o9_07790', [11, 3, 3, 2, 2], 149],
 ['o9_07893', [12, 5, 4, 3, 2], 200],
 ['o9_07943', [7, 7, 7, 3], 160],
 ['o9_07945', [12, 7, 5, 3, 2], 233],
 ['o9_08006', [11, 8, 3, 3, 3], 215],
 ['o9_08042', [7, 7, 7, 4, 3, 3], 184],
 ['o9_08224', [7, 7, 7, 3, 2], 162],
 ['o9_08302', [7, 7, 7, 4, 3, 2, 2], 182],
 ['o9_08477', [4, 4, 4, 4, 4, 3, 3], 101],
 ['o9_08497', [7, 5], 79],
 ['o9_08647', [14, 5, 5, 4, 2, 2], 272],
 ['o9_08765', [7, 7, 7, 4, 2], 169],
 ['o9_08771', [14, 9, 5, 3, 2], 317],
 ['o9_08776', [14, 6, 5, 3, 2], 272],
 ['o9_08828', [13, 5, 5, 3, 3], 240],
 ['o9_08831', [7, 7, 7, 3, 3, 2, 2], 175],
 ['o9_08852', [14, 8, 6, 3, 3], 317],
 ['o9_08875', [13, 8, 5, 2, 2], 268],
 ['o9_09052', [5, 4, 4, 4], 77],
 ['o9_09213', [5, 5, 5, 5, 5, 4, 2, 2], 151],
 ['o9_09372', [10, 4, 4], 136],
 ['o9_09465', [13, 4, 4, 3, 2], 216],
 ['o9_09808', [13, 9, 4, 4, 2, 2], 292],
 ['o9_10020', [3, 3, 3, 3, 3, 2, 2, 2], 59],
 ['o9_10696', [9, 4], 102],
 ['o9_11002', [8, 6, 2], 108],
 ['o9_11100', [9, 5, 3], 118],
 ['o9_11248', [11, 4, 4, 4], 173],
 ['o9_11467', [11, 11, 5, 3, 3], 288],
 ['o9_11537', [6, 6, 6, 4], 128],
 ['o9_11541', [4, 3, 3, 3, 3, 3], 64],
 ['o9_11560', [11, 11, 6, 5, 3, 2], 318],
 ['o9_11570', [11, 3, 3, 3, 3], 160],
 ['o9_11685', [10, 3, 3, 3, 2, 2], 137],
 ['o9_11795', [10, 3, 3, 2], 124],
 ['o9_11845', [8, 7, 2, 2, 2, 2], 131],
 ['o9_11999', [13, 7, 5, 2, 2], 253],
 ['o9_12144', [10, 9, 3, 3, 3], 211],
 ['o9_12230', [11, 9, 3, 3, 3], 232],
 ['o9_12412', [10, 7, 3, 2], 164],
 ['o9_12459', [8, 7, 4, 4], 149],
 ['o9_12519', [5, 5, 5, 5, 4, 3, 2], 131],
 ['o9_12693', [5, 5, 5, 4, 4], 111],
 ['o9_12736', [9, 8, 4, 4], 181],
 ['o9_12757', [5, 5, 5, 5, 5, 3, 3], 146],
 ['o9_12873', [14, 5, 5, 3, 2], 261],
 ['o9_12892', [11, 4, 4, 3, 2, 2], 172],
 ['o9_12919', [11, 5, 4, 2], 168],
 ['o9_12971', [6, 6, 6, 5, 3, 3], 154],
 ['o9_13052', [8, 8, 5, 4], 173],
 ['o9_13056', [11, 8, 4, 4], 221],
 ['o9_13125', [10, 7, 4, 3], 177],
 ['o9_13182', [6, 6, 6, 5, 2, 2, 2], 147],
 ['o9_13188', [6, 6, 6, 6, 4, 3], 172],
 ['o9_13400', [8, 8, 7, 2, 2, 2], 191],
 ['o9_13403', [11, 7, 4, 2], 192],
 ['o9_13433', [12, 5, 5, 3, 2], 209],
 ['o9_13508', [13, 6, 4, 3], 233],
 ['o9_13537', [11, 6, 5, 2, 2, 2], 196],
 ['o9_13604', [6, 6, 6, 6, 5, 2, 2], 179],
 ['o9_13639', [8, 8, 6, 3, 2], 179],
 ['o9_13649', [11, 4, 4, 2], 159],
 ['o9_13666', [11, 7, 3, 3], 191],
 ['o9_13720', [10, 10, 4, 4, 3], 244],
 ['o9_13952', [13, 5, 5, 2, 2], 229],
 ['o9_14018', [13, 7, 6, 3, 3], 275],
 ['o9_14079', [13, 4, 4, 4, 2, 2], 227],
 ['o9_14108', [9, 4, 3], 109],
 ['o9_14136', [9, 5, 4, 4], 142],
 ['o9_14359', [9, 7, 3, 2, 2], 149],
 ['o9_14364', [7, 7, 6, 2, 2], 144],
 ['o9_14376', [10, 10, 6, 3, 3], 257],
 ['o9_14495', [10, 7, 3, 3, 2, 2], 177],
 ['o9_14599', [13, 6, 6, 2, 2, 2], 255],
 ['o9_14716', [7, 7, 7, 6, 2, 2, 2], 197],
 ['o9_14831', [8, 3, 2], 80],
 ['o9_14974', [11, 8, 3, 2, 2], 204],
 ['o9_15506', [11, 7, 4, 3, 2, 2], 205],
 ['o9_15633', [12, 7, 4, 3, 2], 224],
 ['o9_15808', [7, 3, 2, 2, 2], 72],
 ['o9_15997', [13, 9, 4, 3, 2], 281],
 ['o9_16065', [14, 9, 5, 4, 2, 2], 328],
 ['o9_16141', [11, 11, 5, 5, 2, 2], 302],
 ['o9_16157', [9, 9, 9, 5, 3, 2], 283],
 ['o9_16181', [13, 8, 5, 3, 3], 279],
 ['o9_16319', [9, 9, 9, 4, 4, 2, 2], 285],
 ['o9_16356', [8, 8, 8, 3, 3, 3], 222],
 ['o9_16527', [8, 8, 8, 5, 2, 2], 227],
 ['o9_16642', [11, 11, 6, 4, 2, 2], 304],
 ['o9_16685', [3, 3, 2, 2, 2, 2, 2, 2], 44],
 ['o9_16748', [7, 7, 7, 5, 3, 2], 187],
 ['o9_16920', [8, 5, 3, 3, 2], 113],
 ['o9_17450', [11, 6, 4, 2], 179],
 ['o9_18007', [7, 7, 6, 4, 3], 162],
 ['o9_18209', [7, 7, 7, 4, 4], 183],
 ['o9_18341', [3, 3, 3, 3, 2, 2, 2, 2], 54],
 ['o9_18633', [11, 5, 5, 2, 2, 2], 185],
 ['o9_18646', [5, 5, 3, 2, 2, 2], 73],
 ['o9_18813', [9, 6, 4, 2], 139],
 ['o9_19130', [7, 6, 5, 2, 2], 120],
 ['o9_19364', [3, 3, 3, 2, 2, 2, 2, 2], 49],
 ['o9_19396', [4, 3, 3, 3, 3, 2], 58],
 ['o9_19724', [10, 4, 3, 3, 2], 140],
 ['o9_20219', [10, 8, 3, 3, 2], 188],
 ['o9_20305', [6, 5, 4], 81],
 ['o9_20364', [9, 6, 2, 2, 2], 131],
 ['o9_20472', [9, 5, 4, 3], 134],
 ['o9_21195', [8, 7, 3, 3], 134],
 ['o9_21513', [10, 4, 3, 2], 131],
 ['o9_21893', [7, 4, 4, 3], 93],
 ['o9_21918', [5, 5, 5, 3, 3, 2], 99],
 ['o9_22129', [10, 3, 3], 122],
 ['o9_22477', [8, 3, 3, 3, 2], 97],
 ['o9_22607', [9, 5], 111],
 ['o9_22663', [9, 5, 5, 2, 2], 141],
 ['o9_22698', [9, 9, 4, 2, 2], 188],
 ['o9_22925', [6, 6, 5, 4, 2, 2], 123],
 ['o9_23023', [9, 9, 5, 4, 3, 2], 218],
 ['o9_23179', [6, 5, 5, 3, 2], 101],
 ['o9_23263', [11, 4, 4, 3, 3], 174],
 ['o9_23660', [11, 7, 4], 190],
 ['o9_23955', [7, 7, 7, 4], 167],
 ['o9_23961', [10, 7, 3, 3, 3], 179],
 ['o9_23971', [5, 4, 4, 4, 2, 2], 83],
 ['o9_23977', [9, 8, 3, 3, 3], 175],
 ['o9_24149', [7, 7, 7, 3, 3, 3], 177],
 ['o9_24183', [14, 8, 5, 3, 2], 300],
 ['o9_24290', [5, 5, 2, 2, 2, 2], 68],
 ['o9_24401', [5, 4, 2, 2, 2], 55],
 ['o9_24534', [9, 4, 4, 4], 133],
 ['o9_24592', [8, 5, 2], 96],
 ['o9_24779', [5, 5, 5, 4, 3], 103],
 ['o9_24886', [14, 6, 6, 3, 3], 289],
 ['o9_24889', [9, 9, 7, 3, 3], 232],
 ['o9_25199', [5, 4, 4, 3], 69],
 ['o9_25341', [4, 4, 4, 3, 2, 2, 2], 71],
 ['o9_25444', [4, 4, 4, 3, 3, 3], 78],
 ['o9_25595', [10, 3, 3, 3, 3], 139],
 ['o9_25709', [4, 3, 2, 2, 2, 2], 43],
 ['o9_26141', [9, 4, 4, 3], 125],
 ['o9_26471', [4, 4, 3, 3, 3, 3], 71],
 ['o9_26570', [7, 5, 3, 2, 2], 93],
 ['o9_26604', [9, 6, 4, 2, 2], 143],
 ['o9_26767', [5, 2, 2, 2, 2, 2], 47],
 ['o9_26791', [11, 6, 3, 2], 172],
 ['o9_27155', [11, 5, 3, 2], 161],
 ['o9_27261', [8, 8, 7, 3, 3, 2], 201],
 ['o9_27392', [7, 7, 7, 6, 3, 3], 204],
 ['o9_27429', [10, 6, 3, 2], 151],
 ['o9_27480', [11, 4, 4], 157],
 ['o9_27737', [10, 7, 3], 162],
 ['o9_28113', [6, 6, 6, 6, 5, 3, 2], 184],
 ['o9_28153', [9, 9, 5, 2, 2], 197],
 ['o9_28284', [7, 6, 4, 2, 2], 111],
 ['o9_28529', [13, 7, 4, 3], 246],
 ['o9_28592', [8, 8, 7, 4, 3], 205],
 ['o9_28746', [11, 5, 5, 3, 3], 192],
 ['o9_28810', [9, 9, 4, 4, 3, 2], 209],
 ['o9_29048', [5, 3, 2, 2, 2, 2], 52],
 ['o9_29246', [8, 8, 8, 6, 3, 3], 249],
 ['o9_29436', [9, 9, 8, 3, 3, 2], 250],
 ['o9_29529', [8, 7, 5, 3, 2], 153],
 ['o9_30150', [8, 3, 2, 2, 2], 87],
 ['o9_30375', [11, 6, 5, 3, 3], 203],
 ['o9_30721', [7, 7, 4, 4, 2], 136],
 ['o9_30790', [13, 6, 6, 3, 3], 262],
 ['o9_31165', [11, 7, 4, 3, 3], 207],
 ['o9_31267', [7, 4, 3, 3, 2], 89],
 ['o9_31321', [4, 3, 3, 3, 3, 2, 2], 62],
 ['o9_31481', [7, 4, 2, 2, 2], 79],
 ['o9_32132', [7, 5, 3], 86],
 ['o9_32150', [4, 4, 4, 4, 3, 3, 2], 88],
 ['o9_32257', [7, 6, 3], 97],
 ['o9_32471', [5, 5, 3, 3, 2, 2], 78],
 ['o9_32588', [5, 5, 4, 3, 2, 2], 85],
 ['o9_33189', [4, 4, 4, 3, 3, 2, 2], 76],
 ['o9_33284', [7, 7, 6, 3, 2], 149],
 ['o9_33526', [7, 4, 4, 2, 2], 91],
 ['o9_33585', [8, 6, 3, 3, 2], 124],
 ['o9_34000', [7, 6, 3, 3, 2], 109],
 ['o9_34403', [8, 6, 3], 112],
 ['o9_35320', [6, 6, 5, 4, 2], 119],
 ['o9_35549', [11, 11, 5, 5, 3, 2], 307],
 ['o9_35666', [5, 5, 4, 4, 2, 2], 92],
 ['o9_35682', [6, 6, 5, 3], 109],
 ['o9_35736', [11, 11, 6, 3, 3], 299],
 ['o9_35772', [6, 6, 4, 3, 3], 109],
 ['o9_35928', [4, 4, 3, 3, 3, 2], 65],
 ['o9_36114', [7, 6, 4, 2], 107],
 ['o9_36250', [5, 4, 4, 4, 3, 2], 88],
 ['o9_37050', [10, 6, 3, 3, 2], 160],
 ['o9_37291', [6, 5, 5, 3, 3], 107],
 ['o9_37685', [5, 3, 3, 3, 3], 64],
 ['o9_37751', [7, 3, 3, 3, 2], 82],
 ['o9_37754', [6, 6, 4, 3, 2], 103],
 ['o9_37851', [8, 5, 2, 2, 2], 103],
 ['o9_37941', [6, 6, 5, 3, 3, 2], 121],
 ['o9_38811', [6, 5, 3, 2, 2], 80],
 ['o9_38989', [5, 5, 4, 4, 2], 88],
 ['o9_39394', [8, 7, 4, 2, 2], 139],
 ['o9_39451', [7, 6, 3, 2, 2], 104],
 ['o9_39521', [6, 6, 5, 5, 2, 2], 132],
 ['o9_39606', [4, 4, 3, 3, 3, 2, 2], 69],
 ['o9_39608', [5, 3, 3, 3, 3, 2], 67],
 ['o9_39879', [5, 3, 3, 3, 2, 2], 62],
 ['o9_39981', [5, 3, 3, 2, 2, 2], 57],
 ['o9_40075', [5, 5, 4, 4, 3, 2], 97],
 ['o9_40179', [8, 7, 3, 2, 2], 132],
 ['o9_40504', [6, 3, 2, 2, 2], 59],
 ['o9_41372', [6, 5, 3, 3, 3], 91],
 ['o9_42224', [5, 5, 3, 3, 3, 2], 83],
 ['o9_43001', [8, 5, 4, 2, 2], 115],
 ['o9_43679', [7, 7, 5, 3, 3], 144],
 ['o9_43953', [9, 4, 3, 3], 118],
 ['o9_44054', [9, 5, 3, 3], 127],
 ['s042', [5, 5, 2], 57],
 ['s068', [5, 5, 3, 2, 2], 69],
 ['s086', [3, 3, 3, 3, 2, 2], 46],
 ['s104', [7, 3, 2, 2], 68],
 ['s114', [7, 4, 3, 2], 80],
 ['s294', [5, 4, 2], 47],
 ['s301', [5, 5, 3], 62],
 ['s308', [5, 5, 2, 2, 2], 64],
 ['s336', [4, 4, 3, 2, 2], 51],
 ['s344', [6, 4, 3], 64],
 ['s346', [7, 3, 3, 2], 73],
 ['s367', [4, 4, 4, 3, 2], 63],
 ['s369', [6, 5, 2, 2], 71],
 ['s384', [3, 2, 2, 2, 2], 27],
 ['s407', [7, 4, 2, 2], 75],
 ['s582', [4, 4, 3, 3], 53],
 ['s652', [3, 3, 2, 2, 2], 32],
 ['s665', [5, 5, 4, 2, 2], 76],
 ['s684', [5, 4, 3, 2], 56],
 ['s769', [6, 5, 3, 2], 76],
 ['s800', [5, 5, 3, 3], 71],
 ['s849', [4, 3, 3, 2], 40],
 ['t00110', [5, 5, 5, 5, 2], 107],
 ['t00146', [5, 5, 5, 5, 3, 2, 2], 119],
 ['t00324', [3, 3, 3, 3, 3, 3, 2, 2], 64],
 ['t00423', [7, 7, 7, 3, 2, 2], 166],
 ['t00434', [7, 7, 7, 4, 3, 2], 178],
 ['t00550', [6, 6, 2], 80],
 ['t00729', [7, 7, 2, 2], 109],
 ['t00787', [7, 7, 5, 2, 2, 2], 137],
 ['t00826', [8, 8, 3, 3, 2, 2], 156],
 ['t00855', [8, 8, 5, 3], 165],
 ['t00873', [8, 8, 3, 2, 2], 147],
 ['t00932', [8, 8, 5, 3, 3], 174],
 ['t01033', [5, 5, 5, 5, 3], 112],
 ['t01037', [5, 5, 5, 5, 2, 2, 2], 114],
 ['t01125', [10, 3, 3, 2, 2], 128],
 ['t01216', [10, 4, 3, 3], 137],
 ['t01268', [10, 7, 3, 3, 2], 173],
 ['t01292', [10, 6, 4, 3], 164],
 ['t01318', [9, 4, 3, 2, 2], 116],
 ['t01368', [9, 5, 4, 2], 128],
 ['t01409', [9, 9, 4, 3, 2], 193],
 ['t01422', [4, 4, 4, 4, 3, 2, 2], 83],
 ['t01424', [9, 9, 5, 4, 2, 2], 213],
 ['t01440', [4, 4, 4, 4, 4, 3, 2], 95],
 ['t01598', [11, 5, 4, 2, 2], 172],
 ['t01636', [11, 4, 4, 3, 2], 168],
 ['t01646', [11, 6, 5, 2, 2], 192],
 ['t01690', [11, 7, 4, 2, 2], 196],
 ['t01757', [7, 7, 2, 2, 2, 2], 116],
 ['t01815', [6, 5, 2], 68],
 ['t01834', [7, 7, 5, 2], 130],
 ['t01850', [8, 5, 4], 109],
 ['t01863', [10, 3, 3, 3, 2], 133],
 ['t01949', [8, 7, 2, 2, 2], 127],
 ['t02099', [5, 5, 5, 4, 2], 97],
 ['t02104', [9, 4, 4, 2], 119],
 ['t02238', [8, 8, 3, 3], 149],
 ['t02276', [3, 2, 2, 2, 2, 2, 2], 35],
 ['t02378', [11, 4, 4, 2, 2], 163],
 ['t02398', [8, 8, 5, 3, 2, 2], 172],
 ['t02404', [9, 5, 3, 2, 2], 125],
 ['t02470', [10, 7, 3, 2, 2], 168],
 ['t02537', [7, 7, 7, 3, 3, 2], 171],
 ['t02567', [7, 7, 7, 4, 2, 2], 173],
 ['t02639', [11, 7, 4, 3, 2], 201],
 ['t03566', [7, 7, 3], 111],
 ['t03607', [10, 4, 4, 3], 144],
 ['t03709', [7, 7, 4, 3, 3], 135],
 ['t03713', [7, 7, 3, 2], 113],
 ['t03781', [4, 4, 4, 4, 3, 3], 85],
 ['t03864', [7, 7, 4, 3, 2, 2], 133],
 ['t03956', [7, 6, 2, 2], 95],
 ['t03979', [8, 6, 3, 2], 115],
 ['t04003', [7, 7, 4, 2], 120],
 ['t04019', [5, 5, 4, 4], 86],
 ['t04102', [7, 7, 3, 3, 2, 2], 126],
 ['t04180', [5, 5, 5, 5, 4, 2, 2], 126],
 ['t04228', [9, 7, 3, 3], 151],
 ['t04244', [11, 5, 5, 2, 2], 181],
 ['t04382', [10, 6, 3, 3], 157],
 ['t04449', [4, 3, 3, 3, 3], 55],
 ['t04557', [3, 3, 3, 3, 2, 2, 2], 50],
 ['t04721', [7, 7, 6, 2, 2, 2], 148],
 ['t04756', [6, 6, 4], 92],
 ['t05118', [11, 6, 4, 2, 2], 183],
 ['t05239', [11, 5, 3, 3], 167],
 ['t05390', [6, 6, 5, 2, 2, 2], 111],
 ['t05425', [6, 6, 5, 3, 3], 118],
 ['t05426', [11, 6, 5, 3, 2], 197],
 ['t05538', [5, 5, 5, 4, 3, 2], 106],
 ['t05564', [6, 6, 6, 4, 3], 136],
 ['t05578', [9, 8, 3, 3, 2], 169],
 ['t05658', [7, 6, 4, 3], 113],
 ['t05663', [8, 7, 4, 3], 141],
 ['t05674', [6, 6, 6, 5, 2, 2], 143],
 ['t05695', [5, 5, 5, 5, 3, 3], 121],
 ['t06001', [7, 7, 4, 4], 134],
 ['t06440', [8, 8, 3, 3, 3], 158],
 ['t06463', [9, 9, 5, 3, 2], 202],
 ['t06525', [7, 7, 5, 3, 2], 138],
 ['t06570', [8, 8, 5, 2, 2], 163],
 ['t06573', [3, 3, 2, 2, 2, 2, 2], 40],
 ['t06605', [9, 9, 4, 4, 2, 2], 204],
 ['t06715', [5, 3, 2, 2, 2], 48],
 ['t07070', [4, 3, 3, 3, 2], 49],
 ['t07104', [3, 3, 3, 2, 2, 2, 2], 45],
 ['t07348', [6, 5, 4, 2, 2], 87],
 ['t07355', [5, 2, 2, 2, 2], 43],
 ['t07412', [5, 4, 4, 2, 2], 67],
 ['t08111', [5, 5, 3, 3, 2], 74],
 ['t08201', [7, 4, 4, 2], 87],
 ['t08267', [8, 7, 3, 3, 2], 137],
 ['t08403', [9, 4, 2, 2], 107],
 ['t08532', [4, 4, 3, 3, 3], 62],
 ['t08576', [6, 5, 5, 2, 2], 96],
 ['t09016', [9, 5, 4, 3, 2], 137],
 ['t09126', [5, 5, 4, 3], 78],
 ['t09267', [7, 7, 4], 118],
 ['t09313', [7, 7, 6, 3, 3], 155],
 ['t09450', [6, 4, 4], 72],
 ['t09455', [7, 7, 3, 3, 3], 128],
 ['t09500', [4, 4, 3, 2, 2, 2], 55],
 ['t09580', [9, 5, 2, 2], 116],
 ['t09690', [7, 6, 3, 2], 100],
 ['t09704', [8, 8, 6, 3, 3], 185],
 ['t09852', [6, 5, 3], 73],
 ['t09954', [6, 5, 4, 2], 83],
 ['t10188', [5, 4, 3, 2, 2], 60],
 ['t10215', [5, 3, 3, 2, 2], 53],
 ['t10230', [6, 4, 3, 3], 73],
 ['t10262', [5, 3, 3, 3], 55],
 ['t10292', [5, 4, 4, 2], 63],
 ['t10462', [9, 4, 4, 3, 2], 128],
 ['t10643', [6, 6, 6, 5, 3, 2], 148],
 ['t10681', [11, 5, 5, 3, 2], 186],
 ['t10832', [4, 3, 3, 3, 2, 2], 53],
 ['t10985', [11, 6, 3, 3], 178],
 ['t11198', [5, 4, 4, 3, 2], 72],
 ['t11376', [4, 4, 3, 3, 2, 2], 60],
 ['t11548', [4, 4, 4, 3, 3, 2], 72],
 ['t11556', [6, 4, 3, 2], 67],
 ['t11852', [6, 5, 3, 3, 2], 85],
 ['t11909', [5, 3, 3, 3, 2], 58],
 ['t12681', [5, 4, 3, 3], 62],
 ['t12753', [7, 5, 3, 3], 95],
 ['v0082', [5, 5, 5, 2], 82],
 ['v0114', [5, 5, 5, 3, 2, 2], 94],
 ['v0165', [3, 3, 3, 3, 3, 2, 2], 55],
 ['v0220', [7, 7, 3, 2, 2], 117],
 ['v0223', [7, 7, 4, 3, 2], 129],
 ['v0249', [6, 2], 44],
 ['v0330', [7, 2, 2], 60],
 ['v0398', [7, 5, 2, 2, 2], 88],
 ['v0407', [8, 3, 3, 2, 2], 92],
 ['v0424', [8, 3, 2, 2], 83],
 ['v0434', [8, 5, 3], 101],
 ['v0497', [8, 5, 3, 3], 110],
 ['v0554', [7, 2, 2, 2, 2], 67],
 ['v0570', [5, 5, 5, 3], 87],
 ['v0573', [5, 5, 5, 2, 2, 2], 89],
 ['v0707', [4, 4, 4, 3, 2, 2], 67],
 ['v0709', [5, 4, 4], 61],
 ['v0715', [9, 4, 3, 2], 112],
 ['v0740', [4, 4, 4, 4, 3, 2], 79],
 ['v0741', [9, 5, 4, 2, 2], 132],
 ['v0759', [8, 3, 3], 85],
 ['v0765', [7, 5, 2], 81],
 ['v0847', [7, 4, 4], 85],
 ['v0912', [7, 6, 2, 2, 2], 99],
 ['v0939', [5, 5, 4, 2], 72],
 ['v0945', [8, 5, 3, 2, 2], 108],
 ['v0959', [3, 2, 2, 2, 2, 2], 31],
 ['v1077', [7, 7, 3, 3, 2], 122],
 ['v1109', [7, 7, 4, 2, 2], 124],
 ['v1269', [6, 4], 56],
 ['v1300', [7, 3], 62],
 ['v1392', [7, 3, 2], 64],
 ['v1425', [4, 3, 3, 3], 46],
 ['v1547', [7, 4, 2], 71],
 ['v1620', [4, 4, 4, 3, 3], 69],
 ['v1628', [7, 4, 3, 3], 86],
 ['v1690', [7, 4, 3, 2, 2], 84],
 ['v1709', [7, 5, 3, 2], 89],
 ['v1716', [7, 3, 3, 2, 2], 77],
 ['v1718', [8, 3, 3, 3], 94],
 ['v1728', [6, 5, 2, 2, 2], 75],
 ['v1810', [5, 5, 5, 4, 2, 2], 101],
 ['v1832', [6, 5, 3, 3], 82],
 ['v1839', [9, 5, 3, 2], 121],
 ['v1915', [3, 3, 3, 2, 2, 2], 41],
 ['v1921', [8, 5, 2, 2], 99],
 ['v1940', [7, 6, 3, 3], 106],
 ['v1966', [8, 6, 3, 3], 121],
 ['v1980', [5, 3, 3, 2], 49],
 ['v1986', [6, 6, 4, 3], 100],
 ['v2024', [6, 6, 5, 2, 2], 107],
 ['v2090', [9, 4, 4, 2, 2], 123],
 ['v2215', [5, 5, 4, 3, 2], 81],
 ['v2290', [5, 4, 3], 53],
 ['v2325', [5, 5, 5, 3, 3], 96],
 ['v2384', [3, 3, 2, 2, 2, 2], 36],
 ['v2759', [7, 4], 69],
 ['v2925', [4, 3, 2, 2, 2], 39],
 ['v2930', [7, 3, 3, 3], 79],
 ['v3105', [4, 3, 3, 2, 2], 44],
 ['v3354', [6, 6, 5, 3, 2], 112],
 ['v3482', [4, 4, 3, 3, 2], 56]]